
(include-book "../src/acl2/grid")
(include-book "../src/acl2/cell")
(include-book "../src/acl2/avl-utils")
(include-book "generators/grid-data-generator")


;;;The AVL utils module contains methods for manipulating
;;;avl trees. Most of these are functions for nested
;;;avl trees used by the lifelike grids.
;;;Some of these are used very directly by grid methods,
;;; and thus don't have tests here (the grid tests already
;;; exercise them). These are:
;;;  nested-avl-insert - lifelike-grid-set-cell
;;;  nested-avl-delete - lifelike-grid-set-cell



  
 ;;Helper method:
;;Given a list of unique elements uniques, return true
;;iff each member of uniques appears in maybe-repeats
;;1 or more times, and no members of maybe-repeats
;;do not appear in uniques.
(defun has-same-members-with-poss-repeats (uniques maybe-repeats)
	(if (endp uniques)
		(not maybe-repeats)
		(if (member-equal (car uniques) maybe-repeats)
			(has-same-members-with-poss-repeats
				(cdr uniques)
				(remove-equal (car uniques) maybe-repeats))
			nil)))

;;;Test that nested-avl-flatten-to-cells
;;;retrieves all the cells entered into a nested
;;;avl tree. Since a lifelike grid is equivalent
;;;to an avl tree, lifelike grid functions are used
;;;to construct
(defproperty test-flatten-to-cells-returns-cells-inserted
	(some-cells :value (random-list-of (cell (random-integer) 
                                                 (random-integer)))
	 cell-grid :value (lifelike-grid-set-multiple-cells
	 					(empty-lifelike-grid)
	 					some-cells t))
	(has-same-members-with-poss-repeats
		(nested-avl-flatten-to-cells cell-grid) some-cells))


;;verify that avl-min gets the cons pair for the minimum
;;key of an AVL tree and avl-max gets the
;;largest. elementary grid functions are used to create
;;the AVL tree because an elementary grid is equivalent
;;to an AVL tree.
(defproperty avl-min-and-max-get-right-elements
  (lowest-x :value (random-integer)
   biggest-x :value (random-between lowest-x (* 10 (abs lowest-x)))
   tr :value (elementary-grid-set-multiple (empty-elementary-grid)
                (append 
                   (list lowest-x biggest-x)
                   (random-list-of (random-between lowest-x biggest-x)))
                t))
  (and (equal (avl-min tr) (cons lowest-x t))
       (equal (avl-max tr) (cons biggest-x t))))
  